A, B:MsgA. (A ||+ B)  Feasible(A)  Feasible(B)  Feasible(A  B) 

latex

Definitions

ma-frame-compat(A;B), M1  M2, Feasible(M), A ||+ B, ma-frame-compatible(A;B), M1 ||decl M2, M1 || M2, 1of(t), 2of(t), xdom(f). v=f(x)   P(x;v), MsgA, mk-ma, Valtype(da;k), if b t else f fi, union-deq(A;B;a;b), sumdeq(a;b), sum-deq(A;B;a;b), IdLnk, IdLnkDeq, product-deq(A;B;a;b), proddeq(a;b), prod-deq(A;B;a;b), Atom, , {x:A| B(x) }, , AB, a<b, #$n, AtomDeq, atom-deq-aux, NatDeq, <a,b>, nat-deq-aux, T, P  Q, True, AtomFree(T;x), False, Dec(P), x:A. B(x), f(a), f(x), f  g, x:A. B(x), Void, left+right, Unit, P  Q, P & Q, x:AB(x), P  Q, x  dom(f), IdDeq, a:A fp B(a), State(ds), x:AB(x), f(x)?z, x. t(x), x.A(x), Knd, KindDeq, locl(a), Top, Type, Id, Prop, s = t, , b, P  Q, A, b, x:A. B(x), t  T, {T}, s ~ t, f || g, SQType(T)

Lemmas

bool sq, bool cases, fpf-sub-join-right, fpf-ap wf, fpf-join-cap-sq, fpf-sub-join-left, subtype-fpf-cap, subtype rel self, subtype rel dep function, assert wf, not wf, bnot wf, bool wf, Id wf, top wf, locl wf, Kind-deq wf, Knd wf, fpf-cap wf, ma-state wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-join-dom2, fpf-join-ap-sq, fpf-join wf, fpf-join-dom, fpf-join-ap, true wf, squash wf, atom-free wf, decidable wf, ma-join-frame-compat2, ma-join wf, ma-join-frame-compat, msga wf, ma-compat wf, ma-feasible wf